\begin{tabbing}
comp{-}atom{-}ap($g$;$f$;$x$;$a$)
\\[0ex]$\,\equiv$$_{\mbox{\scriptsize def}}$$\;\;$\=let ${\it f'}$ = $\lambda$$a$.$g$$\,\circ\,$$f$ in \+
\\[0ex]let ${\it x'}$ = $\lambda$$a$.$x$ in 
\\[0ex]let $F$ = $\lambda$$b$,$c$. ${\it f'}$($b$,${\it x'}$($c$)) in 
\\[0ex]let $L$ = atoms{-}in($F$) in 
\\[0ex]let $b$ = new{-}atom(($a$.$L$)) in 
\\[0ex]i\=f $F$($b$,$a$)=$_{2}$$a$$\in$Atom$\rightarrow$ inr(${\it f'}$($b$))\+
\\[0ex]; $F$($a$,$b$)=$_{2}$$a$$\in$Atom$\rightarrow$ inl($\lambda$$f$.$g$($f$(${\it x'}$($b$))))
\-\\[0ex]else inr($\lambda$$x$.hd(list{-}diff(AtomDeq;monitor((${\it f'}$($b$,$x$)));$b$.$L$))) fi
\-
\end{tabbing}